| abstract class $ARR{ETP} < $RO_ARR{ETP} |
|---|
| **** | The indices are integers and lie in [0, size-1] Similar to a MAP from ints to elements, but more restrictive conditions The features are repeated here so as to restate the preconditions Inherits: copy, size, capacity, elt! and has size: INT; elt!: ETP; has(e: ETP): BOOL; |
| $RO_ARR{_} | $CONTAINER{_} | $ELT{_} | $ELT |
| $LIST{_} | LIST{_} | A_LIST{_} | ARRAY{_} | FLIST{_} | FSTR |
| aget(i: INT): ETP; |
|---|
| **** | pre has_ind(i) |
| aset(ind: INT,e: ETP); |
|---|
| **** | pre has_ind(i) |
| copy: SAME; |
|---|
| **** | Redefined to narrow the return type |
| has_ind(i: INT): BOOL; |
|---|
| **** | return 0<=i<size This method could actually be implemented at this level |
| ind!: INT; |
|---|
| **** | post 0<=result<size Returns all the indices, which are the integers between 0 and size - 1 |
